*****∀E KW S,P,W;

1 T(KW(S,P),W)≡(T(K(S,P),W)∨T(K(S,NOT(P)),W))  

*****∀E REFLEX S,W;

2 A(S,W,W)  

*****∀E KNOW S,NOT(P),W;

3 T(K(S,NOT(P)),W)≡∀W1.(A(S,W,W1)⊃T(NOT(P),W1))  

*****∀E NOT W,P;

4 T(NOT(P),W)≡¬T(P,W)  

*****ASSUME T(K(S,NOT(P)),W);

5 T(K(S,NOT(P)),W)  (5)

***** 3,5;

6 ∀W1.(A(S,W,W1)⊃T(NOT(P),W1))  (5)

*****∀E ↑ W;

7 A(S,W,W)⊃T(NOT(P),W)  (5)

*****⊃E 2,↑;

8 T(NOT(P),W)  (5)

*****⊃I 5⊃↑;

9 T(K(S,NOT(P)),W)⊃T(NOT(P),W)  

***** 1,4,9;

10 (T(P,W)∧T(KW(S,P),W))⊃T(K(S,P),W)  
*****LABEL (KW1 . 11);

*****∀I ↑ S P W;

11 ∀S P W.((T(P,W)∧T(KW(S,P),W))⊃T(K(S,P),W))  

*****∀E KNOW S,P,W;

12 T(K(S,P),W)≡∀W1.(A(S,W,W1)⊃T(P,W1))  

*****ASSUME T(K(S,P),W);

13 T(K(S,P),W)  (13)

***** 12:13;

14 ∀W1.(A(S,W,W1)⊃T(P,W1))  (13)

*****∀E ↑ W;

15 A(S,W,W)⊃T(P,W)  (13)

*****⊃E 2,↑;

16 T(P,W)  (13)

*****⊃I 13⊃↑;

17 T(K(S,P),W)⊃T(P,W)  
*****LABEL (KNOWTRUE . 18);

*****∀I ↑ S P W;

18 ∀S P W.(T(K(S,P),W)⊃T(P,W))  

*****∀E ↑ FOOL,KW(WISE3,WHITE1),RW;

19 T(K(FOOL,KW(WISE3,WHITE1)),RW)⊃T(KW(WISE3,WHITE1),RW)  

*****∀E ↑↑ FOOL,KW(WISE3,WHITE2),RW;

20 T(K(FOOL,KW(WISE3,WHITE2)),RW)⊃T(KW(WISE3,WHITE2),RW)  

*****∀E 11 WISE3,WHITE1,RW;

21 (T(WHITE1,RW)∧T(KW(WISE3,WHITE1),RW))⊃T(K(WISE3,WHITE1),RW)  

*****∀E 11 WISE3,WHITE2,RW;

22 (T(WHITE2,RW)∧T(KW(WISE3,WHITE2),RW))⊃T(K(WISE3,WHITE2),RW)  

***** WISEMAN6,WISEMAN1,19,21;

23 T(K(WISE3,WHITE1),RW)  

***** WISEMAN7,WISEMAN1,20,22;

24 T(K(WISE3,WHITE2),RW)  
*****LABEL (ASS1 . 25);

*****ASSUME A(WISE3,RW,W1);

25 A(WISE3,RW,W1)  (25)

*****∀E KNOW WISE3,WHITE1,RW;

26 T(K(WISE3,WHITE1),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(WHITE1,W1))  

*****∀E KNOW WISE3,WHITE2,RW;

27 T(K(WISE3,WHITE2),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(WHITE2,W1))  

***** 23,26;

28 ∀W1.(A(WISE3,RW,W1)⊃T(WHITE1,W1))  

***** 24,27;

29 ∀W1.(A(WISE3,RW,W1)⊃T(WHITE2,W1))  

*****∀E ↑↑ W1;

30 A(WISE3,RW,W1)⊃T(WHITE1,W1)  

*****∀E ↑↑ W1;

31 A(WISE3,RW,W1)⊃T(WHITE2,W1)  

*****⊃E 25,↑↑;

32 T(WHITE1,W1)  (25)

*****⊃E 25,↑↑;

33 T(WHITE2,W1)  (25)

*****∀E KNOW WISE3,K(WISE2,NOT(K(WISE1,WHITE1))),RW;

34 T(K(WISE3,K(WISE2,NOT(K(WISE1,WHITE1)))),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(K(WISE2,NOT(K(WISE1,WHITE1))),W1))  

*****∀E KNOW WISE3,NOT(K(WISE2,WHITE2)),RW;

35 T(K(WISE3,NOT(K(WISE2,WHITE2))),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(NOT(K(WISE2,WHITE2)),W1))  

***** WISEMAN9,34;

36 ∀W1.(A(WISE3,RW,W1)⊃T(K(WISE2,NOT(K(WISE1,WHITE1))),W1))  

***** WISEMAN10,35;

37 ∀W1.(A(WISE3,RW,W1)⊃T(NOT(K(WISE2,WHITE2)),W1))  

*****∀E ↑↑ W1;

38 A(WISE3,RW,W1)⊃T(K(WISE2,NOT(K(WISE1,WHITE1))),W1)  

*****∀E ↑↑ W1;

39 A(WISE3,RW,W1)⊃T(NOT(K(WISE2,WHITE2)),W1)  

*****⊃E 25,↑↑;

40 T(K(WISE2,NOT(K(WISE1,WHITE1))),W1)  (25)

*****⊃E 25,↑↑;

41 T(NOT(K(WISE2,WHITE2)),W1)  (25)

*****∀E FOOL FOOL,P,W;

42 T(K(FOOL,P),W)⊃T(K(FOOL,K(FOOL,P)),W)  

*****∀E FOOL S,K(FOOL,P),W;

43 T(K(FOOL,K(FOOL,P)),W)⊃T(K(FOOL,K(S,K(FOOL,P))),W)  

*****∀E 18 FOOL,K(S,K(FOOL,P)),W;

44 T(K(FOOL,K(S,K(FOOL,P))),W)⊃T(K(S,K(FOOL,P)),W)  

***** 42:44;

45 T(K(FOOL,P),W)⊃T(K(S,K(FOOL,P)),W)  
*****LABEL (FOOL2 . 46);

*****∀I ↑ S W P;

46 ∀S W P.(T(K(FOOL,P),W)⊃T(K(S,K(FOOL,P)),W))  

*****∀E KNOW S,K(FOOL,P),W;

47 T(K(S,K(FOOL,P)),W)≡∀W1.(A(S,W,W1)⊃T(K(FOOL,P),W1))  

*****ASSUME T(K(FOOL,P),W);

48 T(K(FOOL,P),W)  (48)

***** 45,47:48;

49 ∀W1.(A(S,W,W1)⊃T(K(FOOL,P),W1))  (48)

*****∀E ↑ W1;

50 A(S,W,W1)⊃T(K(FOOL,P),W1)  (48)

*****⊃I ↑↑↑⊃↑;

51 T(K(FOOL,P),W)⊃(A(S,W,W1)⊃T(K(FOOL,P),W1))  

***** 51;

52 (T(K(FOOL,P),W)∧A(S,W,W1))⊃T(K(FOOL,P),W1)  
*****LABEL (FOOLTRANS . 53);

*****∀I ↑ S P W W1;

53 ∀S P W W1.((T(K(FOOL,P),W)∧A(S,W,W1))⊃T(K(FOOL,P),W1))  

*****∀E ↑ WISE3,KW(WISE1,WHITE2),RW,W1;

54 (T(K(FOOL,KW(WISE1,WHITE2)),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,KW(WISE1,WHITE2)),W1)  

*****∀E ↑↑ WISE3,KW(WISE1,WHITE3),RW,W1;

55 (T(K(FOOL,KW(WISE1,WHITE3)),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,KW(WISE1,WHITE3)),W1)  

*****∀E ↑↑↑ WISE3,KW(WISE2,WHITE1),RW,W1;

56 (T(K(FOOL,KW(WISE2,WHITE1)),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,KW(WISE2,WHITE1)),W1)  

*****∀E 53 WISE3,KW(WISE2,WHITE3),RW,W1;

57 (T(K(FOOL,KW(WISE2,WHITE3)),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,KW(WISE2,WHITE3)),W1)  

*****∀E 53 WISE3,OR(WHITE1,OR(WHITE2,WHITE3)),RW,W1;

58 (T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W1)  

***** WISEMAN2,25,54;

59 T(K(FOOL,KW(WISE1,WHITE2)),W1)  (25)

***** WISEMAN3,25,55;

60 T(K(FOOL,KW(WISE1,WHITE3)),W1)  (25)

***** WISEMAN4,25,56;

61 T(K(FOOL,KW(WISE2,WHITE1)),W1)  (25)

***** WISEMAN5,25,57;

62 T(K(FOOL,KW(WISE2,WHITE3)),W1)  (25)

***** WISEMAN8,25,58;

63 T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W1)  (25)

*****∀E KNOW WISE2,WHITE2,W1;

64 T(K(WISE2,WHITE2),W1)≡∀W.(A(WISE2,W1,W)⊃T(WHITE2,W))  

*****∀E NOT W1,K(WISE2,WHITE2);

65 T(NOT(K(WISE2,WHITE2)),W1)≡¬T(K(WISE2,WHITE2),W1)  

***** 41,64:65;

66 ¬∀W.(A(WISE2,W1,W)⊃T(WHITE2,W))  (25)

*****UNIFY↑;

67 ∃W.¬(A(WISE2,W1,W)⊃T(WHITE2,W))  (25)

*****∃E ↑ (W2);

68 ¬(A(WISE2,W1,W2)⊃T(WHITE2,W2))  (68)

***** 68;

69 A(WISE2,W1,W2)  (68)

***** 68;

70 ¬T(WHITE2,W2)  (68)

*****∀E 18 FOOL,KW(WISE2,WHITE1),W1;

71 T(K(FOOL,KW(WISE2,WHITE1)),W1)⊃T(KW(WISE2,WHITE1),W1)  

*****∀E 11 WISE2,WHITE1,W1;

72 (T(WHITE1,W1)∧T(KW(WISE2,WHITE1),W1))⊃T(K(WISE2,WHITE1),W1)  

*****∀E KNOW WISE2,WHITE1,W1;

73 T(K(WISE2,WHITE1),W1)≡∀W.(A(WISE2,W1,W)⊃T(WHITE1,W))  

***** 32,61,71:73;

74 ∀W.(A(WISE2,W1,W)⊃T(WHITE1,W))  (25)

*****∀E ↑ W2;

75 A(WISE2,W1,W2)⊃T(WHITE1,W2)  (25)

*****⊃E 69,↑;

76 T(WHITE1,W2)  (25 68)

*****∀E KNOW WISE2,NOT(K(WISE1,WHITE1)),W1;

77 T(K(WISE2,NOT(K(WISE1,WHITE1))),W1)≡∀W.(A(WISE2,W1,W)⊃T(NOT(K(WISE1,WHITE1)),W))  

***** 40,77;

78 ∀W.(A(WISE2,W1,W)⊃T(NOT(K(WISE1,WHITE1)),W))  (25)

*****∀E ↑ W2;

79 A(WISE2,W1,W2)⊃T(NOT(K(WISE1,WHITE1)),W2)  (25)

*****⊃E 69,↑;

80 T(NOT(K(WISE1,WHITE1)),W2)  (25 68)

*****∀E 53 WISE2,KW(WISE1,WHITE2),W1,W2;

81 (T(K(FOOL,KW(WISE1,WHITE2)),W1)∧A(WISE2,W1,W2))⊃T(K(FOOL,KW(WISE1,WHITE2)),W2)  

*****∀E 53 WISE2,KW(WISE1,WHITE3),W1,W2;

82 (T(K(FOOL,KW(WISE1,WHITE3)),W1)∧A(WISE2,W1,W2))⊃T(K(FOOL,KW(WISE1,WHITE3)),W2)  

*****∀E 53 WISE2,OR(WHITE1,OR(WHITE2,WHITE3)),W1,W2;

83 (T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W1)∧A(WISE2,W1,W2))⊃T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W2)  

*****∀E 18 FOOL,KW(WISE1,WHITE2),W2;

84 T(K(FOOL,KW(WISE1,WHITE2)),W2)⊃T(KW(WISE1,WHITE2),W2)  

*****∀E 18 FOOL,KW(WISE1,WHITE3),W2;

85 T(K(FOOL,KW(WISE1,WHITE3)),W2)⊃T(KW(WISE1,WHITE3),W2)  

***** 59,68,81,84;

86 T(KW(WISE1,WHITE2),W2)  (25 68)

***** 60,68,82,85;

87 T(KW(WISE1,WHITE3),W2)  (25 68)

***** 63,68,83;

88 T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W2)  (25 68)

*****∀E KW WISE1,WHITE2,W2;

89 T(KW(WISE1,WHITE2),W2)≡(T(K(WISE1,WHITE2),W2)∨T(K(WISE1,NOT(WHITE2)),W2))  

*****∀E 18 WISE1,WHITE2,W2;

90 T(K(WISE1,WHITE2),W2)⊃T(WHITE2,W2)  

***** 70,86,89:90;

91 T(K(WISE1,NOT(WHITE2)),W2)  (25 68)

*****∀E KNOW WISE1,WHITE1,W2;

92 T(K(WISE1,WHITE1),W2)≡∀W1.(A(WISE1,W2,W1)⊃T(WHITE1,W1))  

*****∀E NOT W2,K(WISE1,WHITE1);

93 T(NOT(K(WISE1,WHITE1)),W2)≡¬T(K(WISE1,WHITE1),W2)  

***** 80,92:93;

94 ¬∀W1.(A(WISE1,W2,W1)⊃T(WHITE1,W1))  (25 68)

*****UNIFY↑;

95 ∃W1.¬(A(WISE1,W2,W1)⊃T(WHITE1,W1))  (25 68)

*****∃E ↑ (W3);

96 ¬(A(WISE1,W2,W3)⊃T(WHITE1,W3))  (96)

***** 96;

97 A(WISE1,W2,W3)  (96)

***** 96;

98 ¬T(WHITE1,W3)  (96)

*****∀E KNOW WISE1,NOT(WHITE2),W2;

99 T(K(WISE1,NOT(WHITE2)),W2)≡∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE2),W1))  

***** 91,99;

100 ∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE2),W1))  (25 68)

*****∀E ↑ W3;

101 A(WISE1,W2,W3)⊃T(NOT(WHITE2),W3)  (25 68)

*****∀E NOT W3,WHITE2;

102 T(NOT(WHITE2),W3)≡¬T(WHITE2,W3)  

***** 97,101:102;

103 ¬T(WHITE2,W3)  (25 68 96)

*****∀E 53 WISE1,OR(WHITE1,OR(WHITE2,WHITE3)),W2,W3;

104 (T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W2)∧A(WISE1,W2,W3))⊃T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W3)  

***** 88,97,104;

105 T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W3)  (25 68 96)

*****∀E 18 FOOL,OR(WHITE1,OR(WHITE2,WHITE3)),W3;

106 T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W3)⊃T(OR(WHITE1,OR(WHITE2,WHITE3)),W3)  

*****∀E OR W3,WHITE1,OR(WHITE2,WHITE3);

107 T(OR(WHITE1,OR(WHITE2,WHITE3)),W3)≡(T(WHITE1,W3)∨T(OR(WHITE2,WHITE3),W3))  

*****∀E OR W3,WHITE2,WHITE3;

108 T(OR(WHITE2,WHITE3),W3)≡(T(WHITE2,W3)∨T(WHITE3,W3))  

***** 98,103,105:108;

109 T(WHITE3,W3)  (25 68 96)

*****∀E KW WISE1,WHITE3,W2;

110 T(KW(WISE1,WHITE3),W2)≡(T(K(WISE1,WHITE3),W2)∨T(K(WISE1,NOT(WHITE3)),W2))  

*****∀E KNOW WISE1,NOT(WHITE3),W2;

111 T(K(WISE1,NOT(WHITE3)),W2)≡∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE3),W1))  

*****ASSUME ∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE3),W1));

112 ∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE3),W1))  (112)

*****∀E ↑ W3;

113 A(WISE1,W2,W3)⊃T(NOT(WHITE3),W3)  (112)

*****∀E NOT W3,WHITE3;

114 T(NOT(WHITE3),W3)≡¬T(WHITE3,W3)  

***** 97,109,113:114;

115 FALSE  (25 68 112)

*****⊃I 112⊃↑;

116 ∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE3),W1))⊃FALSE  (25 68)

***** 87,110:111,116;

117 T(K(WISE1,WHITE3),W2)  (25 68)

*****∀E 18 WISE1,WHITE3,W2;

118 T(K(WISE1,WHITE3),W2)⊃T(WHITE3,W2)  

*****⊃E ↑↑,↑;

119 T(WHITE3,W2)  (25 68)

*****∀E 18 FOOL,KW(WISE2,WHITE3),W1;

120 T(K(FOOL,KW(WISE2,WHITE3)),W1)⊃T(KW(WISE2,WHITE3),W1)  

*****∀E KW WISE2,WHITE3,W1;

121 T(KW(WISE2,WHITE3),W1)≡(T(K(WISE2,WHITE3),W1)∨T(K(WISE2,NOT(WHITE3)),W1))  

*****∀E KNOW WISE2,NOT(WHITE3),W1;

122 T(K(WISE2,NOT(WHITE3)),W1)≡∀W.(A(WISE2,W1,W)⊃T(NOT(WHITE3),W))  

*****ASSUME ∀W.(A(WISE2,W1,W)⊃T(NOT(WHITE3),W));

123 ∀W.(A(WISE2,W1,W)⊃T(NOT(WHITE3),W))  (123)

*****∀E ↑ W2;

124 A(WISE2,W1,W2)⊃T(NOT(WHITE3),W2)  (123)

*****∀E NOT W2,WHITE3;

125 T(NOT(WHITE3),W2)≡¬T(WHITE3,W2)  

***** 69,119,124:125;

126 FALSE  (25 123)

*****⊃I 123⊃↑;

127 ∀W.(A(WISE2,W1,W)⊃T(NOT(WHITE3),W))⊃FALSE  (25)

***** 62,120:122,127;

128 T(K(WISE2,WHITE3),W1)  (25)

*****∀E 18 WISE2,WHITE3,W1;

129 T(K(WISE2,WHITE3),W1)⊃T(WHITE3,W1)  

*****⊃E ↑↑,↑;

130 T(WHITE3,W1)  (25)

*****⊃I 25⊃↑;

131 A(WISE3,RW,W1)⊃T(WHITE3,W1)  

*****∀I ↑ W1;

132 ∀W1.(A(WISE3,RW,W1)⊃T(WHITE3,W1))  

*****∀E KNOW WISE3,WHITE3,RW;

133 T(K(WISE3,WHITE3),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(WHITE3,W1))  

***** 132:133;

134 T(K(WISE3,WHITE3),RW)